0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 81 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 9 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
delminA_in_gaa(tree(T6, void, T7), T6, T7) → delminA_out_gaa(tree(T6, void, T7), T6, T7)
delminA_in_gaa(tree(T26, tree(T42, void, T43), T28), T42, tree(T26, T43, T31)) → delminA_out_gaa(tree(T26, tree(T42, void, T43), T28), T42, tree(T26, T43, T31))
delminA_in_gaa(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31)) → U1_gaa(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_in_gaa(T57, T62, T63))
U1_gaa(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_out_gaa(T57, T62, T63)) → delminA_out_gaa(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
delminA_in_gaa(tree(T6, void, T7), T6, T7) → delminA_out_gaa(tree(T6, void, T7), T6, T7)
delminA_in_gaa(tree(T26, tree(T42, void, T43), T28), T42, tree(T26, T43, T31)) → delminA_out_gaa(tree(T26, tree(T42, void, T43), T28), T42, tree(T26, T43, T31))
delminA_in_gaa(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31)) → U1_gaa(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_in_gaa(T57, T62, T63))
U1_gaa(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_out_gaa(T57, T62, T63)) → delminA_out_gaa(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31))
DELMINA_IN_GAA(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31)) → U1_GAA(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_in_gaa(T57, T62, T63))
DELMINA_IN_GAA(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31)) → DELMINA_IN_GAA(T57, T62, T63)
delminA_in_gaa(tree(T6, void, T7), T6, T7) → delminA_out_gaa(tree(T6, void, T7), T6, T7)
delminA_in_gaa(tree(T26, tree(T42, void, T43), T28), T42, tree(T26, T43, T31)) → delminA_out_gaa(tree(T26, tree(T42, void, T43), T28), T42, tree(T26, T43, T31))
delminA_in_gaa(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31)) → U1_gaa(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_in_gaa(T57, T62, T63))
U1_gaa(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_out_gaa(T57, T62, T63)) → delminA_out_gaa(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31))
DELMINA_IN_GAA(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31)) → U1_GAA(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_in_gaa(T57, T62, T63))
DELMINA_IN_GAA(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31)) → DELMINA_IN_GAA(T57, T62, T63)
delminA_in_gaa(tree(T6, void, T7), T6, T7) → delminA_out_gaa(tree(T6, void, T7), T6, T7)
delminA_in_gaa(tree(T26, tree(T42, void, T43), T28), T42, tree(T26, T43, T31)) → delminA_out_gaa(tree(T26, tree(T42, void, T43), T28), T42, tree(T26, T43, T31))
delminA_in_gaa(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31)) → U1_gaa(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_in_gaa(T57, T62, T63))
U1_gaa(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_out_gaa(T57, T62, T63)) → delminA_out_gaa(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31))
DELMINA_IN_GAA(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31)) → DELMINA_IN_GAA(T57, T62, T63)
delminA_in_gaa(tree(T6, void, T7), T6, T7) → delminA_out_gaa(tree(T6, void, T7), T6, T7)
delminA_in_gaa(tree(T26, tree(T42, void, T43), T28), T42, tree(T26, T43, T31)) → delminA_out_gaa(tree(T26, tree(T42, void, T43), T28), T42, tree(T26, T43, T31))
delminA_in_gaa(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31)) → U1_gaa(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_in_gaa(T57, T62, T63))
U1_gaa(T26, T56, T57, T58, T28, T62, T63, T61, T31, delminA_out_gaa(T57, T62, T63)) → delminA_out_gaa(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31))
DELMINA_IN_GAA(tree(T26, tree(T56, T57, T58), T28), T62, tree(T26, tree(T56, T63, T61), T31)) → DELMINA_IN_GAA(T57, T62, T63)
DELMINA_IN_GAA(tree(T26, tree(T56, T57, T58), T28)) → DELMINA_IN_GAA(T57)
From the DPs we obtained the following set of size-change graphs: